…tput

…ring

Eliminates the `surj_factor` axiom by providing a complete proof using:
- `finFree_isDiscrete` (follows from `isColimitLocallyConstantPresheafDiagram`)
- `finFree_isColimit_at` (follows from `CondensedMod.isDiscrete_tfae`)
- `Types.jointly_surjective_of_isColimit` (Mathlib colimit machinery)
- `Condensed.freeForgetAdjunction` (existing adjunction)

New imports: Condensed.Discrete.Characterization, Condensed.Discrete.Colimit,
CategoryTheory.Limits.Types.Colimits, CategoryTheory.Types.Basic

Remaining axiom: `sol_leftCancel` (requires CompHaus ↔ TopMod equivalence,
Clausen-Scholze Condensed Mathematics Thm 5.8 + Lemma 5.9)

Co-authored-by: Thomas Riepe <thomasriepe@gmail.com>

Replaces the surj_factor axiom with a complete proof using:
- finFree_isDiscrete (via isColimitLocallyConstantPresheafDiagram)
- finFree_isColimit_at (via CondensedMod.isDiscrete_tfae)
- Types.jointly_surjective_of_isColimit
- Condensed.freeForgetAdjunction

Remaining axiom: sol_leftCancel (requires CompHaus <=> TopMod equivalence,
Clausen-Scholze Condensed Mathematics Thm 5.8 + Lemma 5.9)

Co-authored-by: Thomas Riepe <thomasriepe@gmail.com>

…1D7ED)

The previous push corrupted the Unicode identity morphism symbol (𝟙, U+1D7D9,
CategoryTheory.id) to the identity functor symbol (𝟭, U+1D7ED, Functor.id).
This caused 20 type errors since a morphism was expected but a functor was given.

Also fix buildEta constructor to use cast for the Opposite.op_unop rewrite,
matching the original P2_finFree_Solid.lean approach.

Replaces all identity morphism notations with CategoryTheory.id
and NatTrans.id to avoid push_files Unicode corruption of
U+1D7D9 (𝟙, CategoryTheory.id) to U+1D7ED (𝟭, Functor.id).
Also uses simp [Category.id_comp] to avoid the 𝟙 _ ≫ ... pattern.

Two fixes for Mathlib master compatibility:
1. CategoryTheory.id -> CategoryStruct.id (open CategoryTheory makes
   CategoryStruct available; CategoryTheory.id does not exist)
2. F.obj.obj / F.obj.map -> F.val.obj / F.val.map for CondensedSet
   (Sheaf uses .val for underlying presheaf, not .obj)

Replaces all identity morphism notations with CategoryTheory.id
and NatTrans.id to avoid push_files Unicode corruption of
U+1D7D9 (𝟙, CategoryTheory.id) to U+1D7ED (𝟭, Functor.id).
Also uses simp [Category.id_comp] to avoid the 𝟙 _ ≫ ... pattern.

Surj_factor proof exposed API-mismatch with CI Mathlib master (ObjectProperty migration: CondensedSet.obj vs .val). Reverting to clean axiom version.

Changes from prior axiom version:
- NatTrans.id replaces identity morphism notation in profiniteSolidification
- CategoryStruct.id replaces notation in comp_counit lemma
- simp [Category.id_comp] in isSolid_of_isLimit_gen naturality
- Removed 4 unused imports

surj_factor proof exists locally in P2_finFree_Solid.lean (TODO).

The section variable α (profiniteSolidCounit R) is EXPLICIT in
liftOfIsRightKanExtension and liftOfIsRightKanExtension_fac_app.
Correct call order: F'.liftOfIsRightKanExtension α G β (then X for fac_app).

Previous versions incorrectly passed:
  liftOfIsRightKanExtension _ (NatTrans.id ...)  -- α=_, G=NatTrans -- type mismatch
  liftOfIsRightKanExtension_fac_app _ (NatTrans.id _) T -- same error

Also: replace rw [show IsIso _ <-> ...] with apply (isIso_iff_bijective _).mpr
to avoid pattern matching issues with explicitly-parameterized isIso_iff_bijective.

Also: restructure isSolid_of_isLimit_gen injectivity proof to use
explicit simp [Category.assoc] steps instead of congrArg chains.

Five structural fixes based on P2_finFree_Solid.lean (locally compiled):

1. Add iso_counit_sol lemma: finFreeIsoSolid.hom >> solidification.app LT = 𝟙
   Proved via cancel_mono and IsIso.hom_inv_id.

2. Injectivity in profiniteSolid_fintype_isSolid: use calc proof with
   iso_counit_sol (avoids Type mismatch from step1.trans step2 assoc issue).

3. Surjectivity: add surjectivity_from_surj_factor helper with explicit
   step1 + simp [Category.assoc] to handle right-associativity.

4. isSolid_of_isLimit_gen: use show tactic to guide type elaboration
   in injectivity (avoids Application type mismatch with Yoneda types).
   Use change + simp [Category.id_comp] for cone naturality.

5. finFree_isSolid: rewrite via yoneda.mapIso decomposition (avoids
   manual bijectivity; uses infer_instance for IsIso composition).

isIso_iff_bijective {X Y : Type u} (f : X -> Y) takes an explicit
morphism argument, so direct uses of .mp or rw fail.

1. Both instances of rw [isIso_iff_bijective] replaced with
   apply (isIso_iff_bijective _).mpr
   (in profiniteSolid_fintype_isSolid and isSolid_of_isLimit_gen)

2. bijFun: isIso_iff_bijective.mp X replaced with
   (isIso_iff_bijective _).mp X

3. finFree_isSolid: rw [show A = B from ?_] replaced with
   have h_decomp : A = B := by ext g; simp
   rw [h_decomp]
   (avoids tactic rewrite failure with ?_ metavariable pattern)

CI log (job 82889135241, commit 1dd7723) showed exactly:
  Solid.lean:104:8  - rw [IsIso.inv_hom_id,...] in iso_counit_sol
  Solid.lean:106:13 - rw [..., h_inv, IsIso.hom_inv_id] in iso_counit_sol
  Solid.lean:114:59 - rw [..., Category.comp_id] in sol_map_counit

Fixes:
1. Remove iso_counit_sol entirely (eliminates L104+106 failures).
   The lemma used rw on IsIso.inv_hom_id/hom_inv_id whose patterns
   failed to match (likely notation mismatch CategoryStruct.id vs 𝟙).

2. sol_map_counit L114: replace rw chain ending in Category.comp_id
   with simp [profiniteSolidification_comp_counit R T].
   Root cause: profiniteSolidification_comp_counit produces
   CategoryStruct.id _ but Category.comp_id pattern uses 𝟙 X.
   simp handles both via its builtin normalization.

3. isSolid_of_isLimit_gen: replace show with change (lint fix).

4. profiniteSolid_fintype_isSolid: congrArg+simp injectivity.

5. finFree_isSolid: explicit bijection (no yoneda.mapIso rw).

…er_instance

…omp_id)

exact Category.comp_id _ in sol_map_counit causes cannot-import-non-module
in Lean 4.32.0-rc1 (builds successfully but .olean marked non-importable).
Reverting to v7-style simp [profiniteSolidification_comp_counit R T] which
generates sorry at that step but keeps the module importable.
finFree_isSolid keeps v9 approach (sol_leftCancel + surjectivity_from_surj_factor).

…ule format)

… corruption fix)